DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2019.7

Eta-Equivalence in Core Dependent Haskell

Authors: Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract

We extend the core semantics for Dependent Haskell with rules for η-equivalence. This semantics is defined by two related calculi, Systems D and DC. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler’s core language FC, is the explicitly-typed analogue of System D, suitable for implementation in GHC. Our work builds on and extends the existing metatheory for these systems developed using the Coq proof assistant.

Cite as

Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-Equivalence in Core Dependent Haskell. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kravchukkirilyuk_et_al:LIPIcs.TYPES.2019.7,
  author =	{Kravchuk-Kirilyuk, Anastasiya and Voizard, Antoine and Weirich, Stephanie},
  title =	{{Eta-Equivalence in Core Dependent Haskell}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{7:1--7:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.7},
  URN =		{urn:nbn:de:0030-drops-130716},
  doi =		{10.4230/LIPIcs.TYPES.2019.7},
  annote =	{Keywords: Dependent types, Haskell, Irrelevance, Eta-equivalence}
}

Search Results

Documents authored by Kravchuk-Kirilyuk, Anastasiya

Eta-Equivalence in Core Dependent Haskell

Abstract

Cite as

Thanks for your feedback!

Could not send message